# 1. parenthesize every sentence into unary function applications, either leftward or rightward
# 2. the type of a sentence in boolean
# 3. thing42:chair, thing23:chair
#    chair is predicate that is true of things that are chairs and false of things that are not
#    chairs
#    the type of a noun is thing->boolean
# 4. A N --> A(N)
#    D N --> D(N)
#    N PP ---> PP(N)
#    NP VP --> VP(NP)
#    P NP --> P(NP)
# 5. Every word is going to be modeled as a lambda expression.

primitive type boolean
primitive type thing
typedef N = thing->boolean = thing->S
typedef A = N->N = (thing->S)->(thing->S) = (thing->boolean)->(thing->boolean)
typedef D = N->NP
typedef P = NP->PP = NP->(N<-N) = NP->((thing->S)<-(thing->S))
          = NP->((thing->boolean)<-(thing->boolean))
typedef Vintrans = VP = S<-NP = boolean<-NP
typedef Vtrans = NP->VP = NP->(S<-NP) = NP->(boolean<-NP)
typedef NP =
typedef VP = S<-NP = boolean<-NP
typedef S = boolean
typedef PP = N<-N = (thing->S)<-(thing->S) = (thing->boolean)<-(thing->boolean)

every = (
    lambda noun: (
        lambda noun1: (
            every(lambda x: noun(x)->noun1(x)))))

some = (
    lambda noun: (
        lambda noun1: (
            some(lambda x: noun(x) and noun1(x)))))

pawn = (lambda x: pawn(x))

square = (lambda x: square(x))

is_on1 = (
    lambda object_np: (
        lambda subject_np: (
            subject_np(lambda x: object_np(lambda y: on(x, y))))))

is_on2 = (
    lambda object_np: (
        lambda subject_np: (
            object_np(lambda y: subject_np(lambda x: on(x, y))))))

# Every pawn is on some square

# Every pawn is_on some square

((Every pawn) (is_on (some square)))

is_on(some(square))(every(pawn))

is_on1(some(square))(every(pawn))

is_on2(some(square))(every(pawn))

every(pawn) =

(
    lambda noun: (
        lambda noun1: (
            every(lambda x: noun(x)->noun1(x)))))
((lambda x: pawn(x))) =

# eta reduce

(
    lambda noun: (
        lambda noun1: (
            every(lambda x: noun(x)->noun1(x)))))
(pawn) =

# beta reduce
        lambda noun1: (
            every(lambda x: pawn(x)->noun1(x)))

some(square) =

(
    lambda noun: (
        lambda noun1: (
            some(lambda x: noun(x) and noun1(x)))))
((lambda x: square(x))) =

# eta reduce

(
    lambda noun: (
        lambda noun1: (
            some(lambda x: noun(x) and noun1(x)))))
(square) =

# beta reduce

        lambda noun1: (
            some(lambda x: square(x) and noun1(x)))

is_on1(some(square)) =

(
    lambda object_np: (
        lambda subject_np: (
            subject_np(lambda x: object_np(lambda y: on(x, y))))))
((lambda noun1: (
            some(lambda x: square(x) and noun1(x))))) =

# beta reduce

        lambda subject_np: (
            subject_np(lambda x: (lambda noun1: (
                                   some(lambda x: square(x) and noun1(x))))
                                 (lambda y: on(x, y)))) =

# alpha rename

        lambda subject_np: (
            subject_np(lambda x: (lambda noun1: (
                                   some(lambda x1: square(x1) and noun1(x1))))
                                 (lambda y: on(x, y)))) =

# beta reduce

        lambda subject_np: (
            subject_np(lambda x: (
                                   some(lambda x1: square(x1) and (lambda y: on(x, y))(x1)))
                                 )) =

# beta reduce

        lambda subject_np: (
            subject_np(lambda x: (
                                   some(lambda x1: square(x1) and on(x, x1)))
                                 )) =

is_on1(some(square))(every(pawn)) =

(
    lambda subject_np: (
        subject_np(lambda x: (
            some(lambda x1: square(x1) and on(x, x1)))
                   )))
(
            lambda noun1: (
            every(lambda x: pawn(x)->noun1(x)))) =

# beta reduce

(
        (
            lambda noun1: (
            every(lambda x: pawn(x)->noun1(x))))
        (lambda x: (
            some(lambda x1: square(x1) and on(x, x1)))
                   )) =

# alpha rename

(
        (
            lambda noun1: (
            every(lambda x: pawn(x)->noun1(x))))
        (lambda x2: (
            some(lambda x1: square(x1) and on(x2, x1)))
                   )) =

# beta reduce

(
    every(lambda x: pawn(x)->((lambda x2: (
        some(lambda x1: square(x1) and on(x2, x1)))
                               )
                              (x)))) =

# beta reduce

every(lambda x: pawn(x)->(some(lambda x1: square(x1) and on(x, x1))))

is_on2(some(square))

is_on2(some(square))(every(pawn))